FDL - Nuprl Lemma : cond_rel_equivalent

Nuprl Lemma : cond_rel_equivalent

T:Type, R, Q:(T

T

), P:(T

).
Trans(T;x,y.Q(x,y))

(

x, y:T. (Q(x,y))

(

(Q(y,x))))

R => Q

(

x, y:T. (P(x) & P(y))

(((R(x,y))

(x = y))

(R(y,x))))

(

x, y:T. (P(x) & P(y))

((R(x,y))

(Q(x,y))))

Definitions P Q, P Q, P & Q, x:A B(x), P Q, left + right, s = t, R1 => R2, P Q, A, Trans(T;x,y.E(x;y)), x:A. B(x), x,y. t(x;y), f(a), x:AB(x), , t T, Type, x f y, SQType(T), {T}, s ~ t, False

Lemmas trans wf, not wf, rel implies wf